T:Type, as:T List, f, g:(T).
T  
 sorted(as)
 (priority-select(f;g;as) = inl(false)  +Unit
 (
 ((aas.g(a) & (b:T. (b  as)  ba  f(b)))) 

latex

Definitions	P & Q, x:A. B(x), sorted(L), (xL.P(x)), t  T, x:A. B(x), b, A, AB, P  Q, Prop, (x  l), x. t(x), P  Q, {i..j}, False, ||as||, i  j < k, l[i], P  Q, Unit, false, priority-select(f;g;as), , S  T, , P  Q, Dec(P), A & B, ij, {T}, SQType(T)
Lemmas	decidable int equal, decidable le, select member, sorted wf, priority-select-property, iff functionality wrt iff, bool wf, priority-select wf, bfalse wf, unit wf, int seg wf, select wf, length wf1, l exists wf, l member wf, le wf, not wf, assert wf